/****************************************************************************
 * Elisa 1.0                                                                *
 *--------------------------------------------------------------------------*
 * Author: Laurent Granvilliers, Vincent Sorin                              *
 * Copyright (c) 2004 Laboratoire d'Informatique de Nantes Atlantique       *
 *--------------------------------------------------------------------------*
 * Elisa is distributed WITHOUT ANY WARRANTY. Read the associated           *
 * COPYRIGHT file for more details.                                         *
 *--------------------------------------------------------------------------*
 * elisa_box_reduction.cpp                                                  *
 ****************************************************************************/

#include <list>
#include "elisa_box_reduction.h"
#include "elisa_time.h"

#ifdef ELISA_PROFILE
elisa::Clock elisa::BoxReduction::ClockBox;
long elisa::BoxReduction::NumCall = 0;
#endif // ELISA_PROFILE

USING_ELISA

//--------------------------------------------------------------------------
// class BoxReduction
//--------------------------------------------------------------------------

// box(1.0e-8)-consistency
double BoxReduction::_StaticPrecision = 1.0e-8;

// improvement factor = 10%
double BoxReduction::_StaticImprove = 0.9;

bool BoxReduction::reductionAlgorithm()
{
	bool result = false;
#ifdef ELISA_PROFILE
	BoxReduction::ClockBox.start();
	++ BoxReduction::NumCall;
#endif // ELISA_PROFILE


	// First evaluation; afer this call, only the expression nodes
	// depending on _v are evaluated
	_test->initSatisfaction();

	if (_test->possibleValue()) {
		_v->saveDomain();
		Bound u = _v->domain().sup(), left, right;

		// Reduction of left bound succeeds?
		if (reduceLeft(left)) {
			_v->setQuietDomain(Interval(left, u));

			// Reduction of right bound succeeds?
			if (reduceRight(right)) {
				result = true;
				_v->restoreDomain();

				// New domain
				Interval I(left, right);
				I.intersect(_v->domain());

				// Is the domain improved enough?
				if (I.width() < _improve * _v->domain().width()) {
					_v->setDomain(I);
				} else {
					_v->setQuietDomain(I);
				}
			}
		}
	}

	if (!result) _v->setEmptyDomain();

#ifdef ELISA_PROFILE
	BoxReduction::ClockBox.stop();
#endif //ELISA_PROFILE

	// Is it idempotent?
	if (_precision == 0.0)
		setInactive();

	return result;
}

bool BoxReduction::reduceLeft(Bound & left) const  // left is the bound to be computed
{
	std::list<Interval> l; // stack of domains used for dichotomous search
	l.push_front(_v->domain());

	while (!l.empty()) {
		_v->setQuietDomain(l.front());
		// Is the domain consistent?
		if (_test->isPossiblySatisfied(*_v)) { //<
			// Is the domain canonical?
			if (_v->domain().isCanonical()) {
				left = _v->domain().inf();
				return true; // domain box-consistent
			} else {
				// Creation of a small interval around the left bound
				Interval aux = Interval(nextUp(_v->domain().inf())) + Interval(_precision);
				Interval Ibound(_v->domain().inf(), aux.sup());
				Ibound.intersect(_v->domain());
				_v->setQuietDomain(Ibound);

				// Is this small interval consistent?
				if (_test->isPossiblySatisfied(*_v)) { //<
					left = _v->domain().inf();
					return true; // left bound box-consistent
				} else {
					// the left bound is inconsistent => bisection
					Interval K(Interval(_v->domain().sup(), l.front().sup()));
					Interval::Pair r;
					//K.split(I, J);
					r = K.split();
					l.pop_front();
					//l.push_front(J);
					//l.push_front(I);
					l.push_front(r.second);
					l.push_front(r.first);
				}
			}
		} else {
			l.pop_front(); // domain inconsistent => removed
		}
	}
	return false; // current domain inconsistent, no quasi-zero
}

bool BoxReduction::reduceRight(Bound & right) const  // right is the bound to be computed
{
	std::list<Interval> l;
	l.push_front(_v->domain());

	while (!l.empty()) {
		_v->setQuietDomain(l.front());

		// Is the domain consistent?
		if (_test->isPossiblySatisfied(*_v)) { //<
			// Is the domain canonical?
			if (_v->domain().isCanonical()) {
				right = _v->domain().sup();
				return true; // domain box-consistent
			} else {
				// Creation of a small interval around the right bound
				Interval aux = Interval(nextDown(_v->domain().sup())) - Interval(_precision);
				Interval Ibound(aux.inf(), _v->domain().sup());
				Ibound.intersect(_v->domain());
				_v->setQuietDomain(Ibound);

				// Is this small interval consistent?
				if (_test->isPossiblySatisfied(*_v)) { //<
					right = _v->domain().sup();
					return true; // right bound box-consistent
				} else {
					// the right bound is inconsistent => bisection
					Interval K = Interval(l.front().inf(), _v->domain().inf());
					Interval::Pair r;
					r = K.split();
					l.pop_front();
					l.push_front(r.first);
					l.push_front(r.second);
				}
			}
		} else {
			l.pop_front(); // domain inconsistent => removed
		}
	}
	return false; // current domain inconsistent, no quasi-zero
}

